Inference at * 
Iof proof for Lemma can-apply-p-lift:


  A, B:Type, P:(A), d:(x:ADec(P(x))), f:({x:A| P(x)} B), x:A.
  (can-apply(p-lift(d;f);x))  P(x) 

latex

 by (RepUR ``can-apply p-lift`` ( 0)) 
CollapseTHEN ((UnivCD) 
CollapseTHENA (Auto)) 

latex

C1: 

C1: 1. A : Type
C1: 2. B : Type
C1: 3. P : A
C1: 4. d : x:ADec(P(x))
C1: 5. f : {x:A| P(x)} B
C1: 6. x : A
C1:   (isl(case d(x) of inl(a) => inl (f(x))  | inr(a) => inr a ))  P(x)
C.

Definitions	p-lift(d;f), can-apply(f;x), b, {x:A| B(x)} , Dec(P), x:A. B(x), x(s), f(a), x:AB(x), , t  T, Type
Lemmas	decidable wf